(set-logic QF_BV)
(declare-fun x0 () Bool)
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 8))
(declare-fun x3 () Bool)
(declare-fun x4 () (_ BitVec 32))
(assert (let ( (?v_12 ((_ zero_extend 24) x2))) (let ((?v_16 (bvadd (bvmul (bvsub ?v_12 (_ bv48 32)) x4) (bvsub x1 (_ bv48 32))))) (and true (bvule (bvsub x2 (_ bv48 8)) (_ bv9 8)) true x3 true (= (_ bv0 32) ?v_16) true x0 true))))
(check-sat)
(exit)
